VERS5 
NIL 
((LISTINDUCTION LISPAX#28) (LISTINDUCTIONDEF LISPAX#32) (SEXPINDUCTION LISPAX#33) (SEXPINDUCTIONDEF LISPAX#34) (HIGH_ORDER_DEFINITION LISPAX#38) (LISTDEF LISPAX#43) (APPENDEF LISPAX#45) (LISTAPPEND LISPAX#46) (ALLPDEF LISPAX#50) (SOMEPDEF LISPAX#51) (MAPCARDEF LISPAX#52) (ALISTDEF LISPAX#55) (MKALIST LISPAX#56) (ASSOCDEF LISPAX#58) (MEMBERDEF LISPAX#61) (MATCH_SORT MATCH#16) (ASSOCIATIVITY MATCH#17) (ASSOCIATIVITY_B MATCH#18) (LEMMA_1 MATCH#19) (L1 MATCH#23) (L2 MATCH#24) (L3 MATCH#25) (L4 MATCH#26) (L5 MATCH#27) (LEMMA_2 MATCH#33) (L10 MATCH#34) (L11 MATCH#35) (L12 MATCH#36) (L13 MATCH#37) (L11A MATCH#42) (L12A MATCH#43) (L15 MATCH#50) (LEMMA_3 MATCH#52) (L21 MATCH#54) (L22 MATCH#56) (L23 MATCH#57) (L24 MATCH#58) (L25 MATCH#59) (L26 MATCH#60) (L27 MATCH#63) (RESULT MATCH#69) (CONS_CAR_CDR LISPAX#26 LISPAX#27) (L14 MATCH#38 MATCH#39 MATCH#40 MATCH#41) (SIMPINFO LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16)) (NIL . (DECL CAR (UNARYNAME: CAR) (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CAR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 950) (UNARY& . CAR)) . LISPAX#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 1 .)(NIL . (DECL CDR (UNARYNAME: CDR) (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CDR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 950) (UNARY& . CDR)) . LISPAX#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 2 .)(NIL . (DECL ATOM (UNARYNAME: ATOM) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ATOM . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . ATOM)) . LISPAX#3 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 3 .)(NIL . (DECL NULL (UNARYNAME: NULL) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((NULL . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . NULL)) . LISPAX#4 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 4 .)(NIL . (DECL LISTP (UNARYNAME: LISTP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((LISTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . LISTP)) . LISPAX#5 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 5 .)(NIL . (DECL ALISTP (UNARYNAME: ALISTP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ALISTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . ALISTP)) . LISPAX#6 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 6 .)(NIL . (DECL SEXP (UNARYNAME: SEXP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((SEXP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . SEXP)) . LISPAX#7 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 7 .)(NIL . (DECL SUBLIS (SYNTYPE: CONSTANT) (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|))) . ((SUBLIS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . MATCH#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . MATCH . NIL . 1 .)(NIL . (DECL MATCH (SYNTYPE: CONSTANT) (TYPE: (TY& . |(GROUND⊗GROUND⊗GROUND)→GROUND|))) . ((MATCH . (|(GROUND⊗GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . MATCH#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . MATCH . NIL . 2 .)(NIL . (DECL ISVAR (SYNTYPE: CONSTANT) (TYPE: (TY& . GROUND→TRUTHVAL)) (UNARYNAME: ISVAR)) . ((ISVAR . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((UNARY& . ISVAR)) . MATCH#3 . NIL . CONSTANT .))) . NIL . NIL . NIL . MATCH . NIL . 3 .)(NIL . (DECL (U V W) (TYPE: (TY& . GROUND)) (SORT: (TM& . LISTP))) . ((W . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) (V . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) (U . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) LISTP) . NIL . NIL . NIL . LISPAX . NIL . 8 .)(NIL . (DECL (X Y Z) (TYPE: (TY& . GROUND)) (SORT: (TM& . SEXP))) . ((Z . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) (Y . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) (X . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) SEXP) . NIL . NIL . NIL . LISPAX . NIL . 9 .)(NIL . (DECL (XA YA ZA) (TYPE: (TY& . GROUND)) (SORT: (TM& . ATOM))) . ((ZA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) (YA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) (XA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) ATOM) . NIL . NIL . NIL . LISPAX . NIL . 10 .)(NIL . (DECL (PHI) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((PHI . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#11 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 11 .)(NIL . (DECL CONS (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (SYNTYPE: CONSTANT) (INFIXNAME: |.|) (PREFIXNAME: CONS) (BINDINGPOWER: 850)) . ((CONS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 850) (PREFIX& . CONS) (INFIX& . |.|)) . LISPAX#12 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 12 .)(NIL . (DECL (P P1 P2) (TYPE: (TY& . GROUND)) (SORT: (TM& . SEXP))) . ((P2 . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . MATCH#4 . NIL . VARIABLE .)) (P1 . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . MATCH#4 . NIL . VARIABLE .)) (P . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . MATCH#4 . NIL . VARIABLE .)) SEXP) . NIL . NIL . NIL . MATCH . NIL . 4 .)(NIL . (DECL (E E1 E2) (TYPE: (TY& . GROUND)) (SORT: (TM& . SEXP))) . ((E2 . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . MATCH#5 . NIL . VARIABLE .)) (E1 . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . MATCH#5 . NIL . VARIABLE .)) (E . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . MATCH#5 . NIL . VARIABLE .)) SEXP) . NIL . NIL . NIL . MATCH . NIL . 5 .)(NIL . (DECL (B B1 B2) (TYPE: (TY& . GROUND)) (SORT: (TM& . ALISTP))) . ((B2 . (GROUND . (SYMBOL& ALISTP NIL) . NIL . NIL . MATCH#6 . NIL . VARIABLE .)) (B1 . (GROUND . (SYMBOL& ALISTP NIL) . NIL . NIL . MATCH#6 . NIL . VARIABLE .)) (B . (GROUND . (SYMBOL& ALISTP NIL) . NIL . NIL . MATCH#6 . NIL . VARIABLE .)) ALISTP) . NIL . NIL . NIL . MATCH . NIL . 6 .)(NIL . (DECL NO (TYPE: (TY& . GROUND)) (SORT: (TM& . ATOM)) (SYNTYPE: CONSTANT)) . ((NO . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . MATCH#7 . NIL . CONSTANT .)) ATOM) . NIL . NIL . NIL . MATCH . NIL . 7 .)(|∀XA.SEXP XA| . (AXIOM (TM& . |∀XA.SEXP XA|)) . (ATOM SEXP ZA YA XA) . NIL . (LISPAX#13) . NIL . LISPAX . NIL . 13 .)(|∀U.SEXP U| . (AXIOM (TM& . |∀U.SEXP U|)) . (LISTP SEXP W V U) . NIL . (LISPAX#14) . NIL . LISPAX . NIL . 14 .)(|∀X U.LISTP X.U| . (AXIOM (TM& . |∀X U.LISTP X.U|)) . (LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#15) . NIL . LISPAX . NIL . 15 .)(|∀U.¬NULL U⊃LISTP CDR U| . (AXIOM (TM& . |∀U.¬NULL U⊃LISTP CDR U|)) . (CDR NULL LISTP W V U) . NIL . (LISPAX#16) . NIL . LISPAX . NIL . 16 .)(|∀U.¬NULL U⊃SEXP CAR U| . (AXIOM (TM& . |∀U.¬NULL U⊃SEXP CAR U|)) . (CAR NULL LISTP SEXP W V U) . NIL . (LISPAX#17) . NIL . LISPAX . NIL . 17 .)(|∀X.¬ATOM X⊃SEXP CAR X| . (AXIOM (TM& . |∀X.¬ATOM X⊃SEXP CAR X|)) . (CAR ATOM SEXP Z Y X) . NIL . (LISPAX#18) . NIL . LISPAX . NIL . 18 .)(|∀X.¬ATOM X⊃SEXP CDR X| . (AXIOM (TM& . |∀X.¬ATOM X⊃SEXP CDR X|)) . (CDR ATOM SEXP Z Y X) . NIL . (LISPAX#19) . NIL . LISPAX . NIL . 19 .)(|∀X Y.SEXP X.Y| . (AXIOM (TM& . |∀X Y.SEXP X.Y|)) . (SEXP Z Y X CONS) . NIL . (LISPAX#20) . NIL . LISPAX . NIL . 20 .)(|∀X Y.¬ATOM X.Y| . (AXIOM (TM& . |∀X Y.¬ATOM X.Y|)) . (ATOM SEXP Z Y X CONS) . NIL . (LISPAX#21) . NIL . LISPAX . NIL . 21 .)(|∀X U.¬NULL X.U| . (AXIOM (TM& . |∀X U.¬NULL X.U|)) . (NULL LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#22) . NIL . LISPAX . NIL . 22 .)(|∀U.NULL U⊃U=NIL| . (AXIOM (TM& . |∀U.NULL U⊃U=NIL|)) . (NULL LISTP W V U) . NIL . (LISPAX#23) . NIL . LISPAX . NIL . 23 .)(|∀X Y.CAR (X.Y)=X| . (AXIOM (TM& . |∀X Y.CAR (X.Y)=X|)) . (CAR SEXP Z Y X CONS) . NIL . (LISPAX#24) . NIL . LISPAX . NIL . 24 .)(|∀X Y.CDR (X.Y)=Y| . (AXIOM (TM& . |∀X Y.CDR (X.Y)=Y|)) . (CDR SEXP Z Y X CONS) . NIL . (LISPAX#25) . NIL . LISPAX . NIL . 25 .)(|∀U.¬NULL U⊃CAR U.CDR U=U| . (AXIOM (TM& . |∀U.¬NULL U⊃CAR U.CDR U=U|)) . (CAR CDR NULL LISTP W V U CONS) . NIL . (LISPAX#26) . NIL . LISPAX . NIL . 26 .)(|∀X.¬ATOM X⊃CAR X.CDR X=X| . (AXIOM (TM& . |∀X.¬ATOM X⊃CAR X.CDR X=X|)) . (CAR CDR ATOM SEXP Z Y X CONS) . NIL . (LISPAX#27) . NIL . LISPAX . NIL . 27 .)(|∀PHI.PHI(NIL)∧(∀X U.PHI(U)⊃PHI(X.U))⊃(∀U.PHI(U))| . (AXIOM (TM& . |∀PHI.PHI(NIL)∧(∀X U.PHI(U)⊃PHI(X.U))⊃(∀U.PHI(U))|)) . (LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#28) . NIL . LISPAX . NIL . 28 .)(NIL . (DECL PARS (TYPE: (TY& . GROUND*))) . ((PARS . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#29 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 29 .)(NIL . (DECL (DF DF1 DF2) (TYPE: (TY& . |(GROUND⊗(GROUND*))→(GROUND*)|))) . ((DF2 . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#30 . NIL . VARIABLE .)) (DF1 . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#30 . NIL . VARIABLE .)) (DF . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#30 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 30 .)(NIL . (DECL NILCASE (TYPE: (TY& . |(GROUND*)→(GROUND*)|))) . ((NILCASE . (|(GROUND*)→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#31 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 31 .)(|∀DF NILCASE DEF.(∃FUN.(∀PARS X U.FUN(NIL,PARS)=NILCASE(PARS)∧ FUN(X.U,PARS)= DEF(X,U,FUN(U,DF(X,PARS)),PARS)))| . (AXIOM (TM& . |∀DF NILCASE DEF.(∃FUN.(∀PARS X U.FUN(NIL,PARS)=NILCASE(PARS)∧ FUN(X.U,PARS)= DEF(X,U,FUN(U,DF(X,PARS)),PARS)))|)) . (LISTP SEXP W V U Z Y X CONS PARS DF2 DF1 DF NILCASE (FUN . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .)) (DEF . (|(GROUND⊗GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .))) . NIL . (LISPAX#32) . NIL . LISPAX . NIL . 32 .)(|∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X.Y))⊃(∀X.PHI(X))| . (AXIOM (TM& . |∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X.Y))⊃(∀X.PHI(X))|)) . (ATOM SEXP Z Y X PHI CONS) . NIL . (LISPAX#33) . NIL . LISPAX . NIL . 33 .)(|∀ATOMCASE DEFSEXP DF1 DF2.(∃FUN.(∀PARS X Y Z.(ATOM Z⊃ FUN(Z,PARS)=ATOMCASE(Z,PARS))∧ FUN(X.Y,PARS)= DEFSEXP(X,Y,FUN(X,DF1(X,Y,PARS)), FUN(Y,DF2(X,Y,PARS)), PARS)))| . (AXIOM (TM& . |∀ATOMCASE DEFSEXP DF1 DF2.(∃FUN.(∀PARS X Y Z.(ATOM Z⊃ FUN(Z,PARS)=ATOMCASE(Z,PARS))∧ FUN(X.Y,PARS)= DEFSEXP(X,Y,FUN(X,DF1(X,Y,PARS)), FUN(Y,DF2(X,Y,PARS)), PARS)))|)) . (ATOM LISTP SEXP W V U Z Y X CONS PARS DF2 DF1 DF NILCASE FUN DEF (DEFSEXP . (|(GROUND⊗GROUND⊗GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#34 . NIL . VARIABLE .)) (ATOMCASE . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#34 . NIL . VARIABLE .))) . NIL . (LISPAX#34) . NIL . LISPAX . NIL . 34 .)(NIL . (DECL (ARB ARB1 ARB2) (TYPE: (TY& . ?ARBITRARY))) . ((ARB2 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#35 . NIL . VARIABLE .)) (ARB1 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#35 . NIL . VARIABLE .)) (ARB . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#35 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 35 .)(NIL . (DECL BIGFUN (TYPE: (TY& . |(GROUND⊗GROUND⊗(@ARB)⊗(@ARB))→(@ARB)|))) . ((BIGFUN . (|(GROUND⊗GROUND⊗(@ARB)⊗(@ARB))→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#36 . NIL . VARIABLE .)) ARB) . NIL . NIL . NIL . LISPAX . NIL . 36 .)(NIL . (DECL (DEFINED_FUN ATOM_FUN) (TYPE: (TY& . |GROUND→(@ARB)|))) . ((ATOM_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .)) (DEFINED_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .)) ARB) . NIL . NIL . NIL . LISPAX . NIL . 37 .)(|∀BIGFUN ATOM_FUN.(∃DEFINED_FUN.(∀X Y.(ATOM X⊃DEFINED_FUN(X)=ATOM_FUN(X))∧ DEFINED_FUN(X.Y)= BIGFUN(X,Y,DEFINED_FUN(X), DEFINED_FUN(Y))))| . (AXIOM (TM& . |∀BIGFUN ATOM_FUN.(∃DEFINED_FUN.(∀X Y.(ATOM X⊃DEFINED_FUN(X)=ATOM_FUN(X))∧ DEFINED_FUN(X.Y)= BIGFUN(X,Y,DEFINED_FUN(X), DEFINED_FUN(Y))))|)) . (ATOM SEXP Z Y X CONS ARB BIGFUN ATOM_FUN DEFINED_FUN) . NIL . (LISPAX#38) . NIL . LISPAX . NIL . 38 .)(NIL . (DECL LIST (TYPE: (TY& . |(GROUND*)→GROUND|)) (SYNTYPE: CONSTANT)) . ((LIST . (|(GROUND*)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#39 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 39 .)(NIL . (DECL LST (TYPE: (TY& . GROUND*))) . ((LST . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#40 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 40 .)(|LIST(())=NIL| . (AXIOM (TM& . |LIST(())=NIL|)) . (LIST) . NIL . (LISPAX#41) . NIL . LISPAX . NIL . 41 .)(|∀LST.LISTP LIST(LST)| . (AXIOM (TM& . |∀LST.LISTP LIST(LST)|)) . (LISTP LIST LST) . NIL . (LISPAX#42) . NIL . LISPAX . NIL . 42 .)(|∀X LST.LIST(X,LST)=X.LIST(LST)| . (AXIOM (TM& . |∀X LST.LIST(X,LST)=X.LIST(LST)|)) . (SEXP Z Y X CONS LIST LST) . NIL . (LISPAX#43) . NIL . LISPAX . NIL . 43 .)(NIL . (DECL APPEND (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (INFIXNAME: *) (BINDINGPOWER: 840)) . ((APPEND . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 840) (INFIX& . *)) . LISPAX#44 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 44 .)(|∀X U V.NIL*V=V∧X.U*V=X.(U*V)| . (DEFAX APPEND (TM& . |∀X U V.NIL*V=V∧X.U*V=X.(U*V)|)) . ((APPEND . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 840) (INFIX& . *)) . LISPAX#45 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#45) . NIL . LISPAX . NIL . 45 .)(|∀U V.LISTP U*V| . (AXIOM (TM& . |∀U V.LISTP U*V|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#46) . NIL . LISPAX . NIL . 46 .)(|∀U.U*NIL=U| . (AXIOM (TM& . |∀U.U*NIL=U|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#47) . NIL . LISPAX . NIL . 47 .)(|∀X V.X.NIL*V=X.V| . (AXIOM (TM& . |∀X V.X.NIL*V=X.V|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#48) . NIL . LISPAX . NIL . 48 .)(NIL . (DECL (ALLP SOMEP) (SYNTYPE: CONSTANT) (TYPE: (TY& . |((@PHI)⊗GROUND)→TRUTHVAL|))) . ((SOMEP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#49 . NIL . CONSTANT .)) (ALLP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#49 . NIL . CONSTANT .)) PHI) . NIL . NIL . NIL . LISPAX . NIL . 49 .)(|∀PHI X U.ALLP(PHI,NIL)∧ALLP(PHI,X.U)=(IF PHI(X) THEN ALLP(PHI,U) ELSE FALSE)| . (DEFAX ALLP (TM& . |∀PHI X U.ALLP(PHI,NIL)∧ALLP(PHI,X.U)=(IF PHI(X) THEN ALLP(PHI,U) ELSE FALSE)|)) . ((ALLP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#50 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X PHI CONS (SOMEP . LISPAX#49)) . NIL . (LISPAX#50) . NIL . LISPAX . NIL . 50 .)(|∀PHI X U.¬SOMEP(PHI,NIL)∧ SOMEP(PHI,X.U)=(IF PHI(X) THEN TRUE ELSE SOMEP(PHI,U))| . (DEFAX SOMEP (TM& . |∀PHI X U.¬SOMEP(PHI,NIL)∧ SOMEP(PHI,X.U)=(IF PHI(X) THEN TRUE ELSE SOMEP(PHI,U))|)) . ((SOMEP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#51 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#51) . NIL . LISPAX . NIL . 51 .)(|∀FN X U.MAPCAR(FN,NIL)=NIL∧MAPCAR(FN,X.U)=FN(X).MAPCAR(FN,U)| . (DEFAX MAPCAR (TM& . |∀FN X U.MAPCAR(FN,NIL)=NIL∧MAPCAR(FN,X.U)=FN(X).MAPCAR(FN,U)|)) . ((MAPCAR . (|((GROUND→GROUND)⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#52 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS (FN . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#52 . NIL . VARIABLE .))) . NIL . (LISPAX#52) . NIL . LISPAX . NIL . 52 .)(NIL . (DECL (ALIST) (TYPE: (TY& . GROUND)) (SORT: (TM& . ALISTP))) . ((ALIST . (GROUND . (SYMBOL& ALISTP NIL) . NIL . NIL . LISPAX#53 . NIL . VARIABLE .)) ALISTP) . NIL . NIL . NIL . LISPAX . NIL . 53 .)(|∀ALIST.LISTP ALIST| . (AXIOM (TM& . |∀ALIST.LISTP ALIST|)) . (LISTP ALISTP ALIST) . NIL . (LISPAX#54) . NIL . LISPAX . NIL . 54 .)(|∀ALIST.¬NULL ALIST⊃¬ATOM CAR ALIST∧ATOM CAR (CAR ALIST)| . (AXIOM (TM& . |∀ALIST.¬NULL ALIST⊃¬ATOM CAR ALIST∧ATOM CAR (CAR ALIST)|)) . (CAR ATOM NULL ALISTP ALIST) . NIL . (LISPAX#55) . NIL . LISPAX . NIL . 55 .)(|∀XA Y ALIST.ALISTP (XA.Y).ALIST| . (AXIOM (TM& . |∀XA Y ALIST.ALISTP (XA.Y).ALIST|)) . (ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST) . NIL . (LISPAX#56) . NIL . LISPAX . NIL . 56 .)(NIL . (DECL ASSOC (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (SYNTYPE: CONSTANT)) . ((ASSOC . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#57 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 57 .)(|∀X XA Y ALIST.ASSOC(X,NIL)=NIL∧ ASSOC(X,(XA.Y).ALIST)=(IF X=XA THEN XA.Y ELSE ASSOC(X,ALIST))| . (DEFAX ASSOC (TM& . |∀X XA Y ALIST.ASSOC(X,NIL)=NIL∧ ASSOC(X,(XA.Y).ALIST)=(IF X=XA THEN XA.Y ELSE ASSOC(X,ALIST))|)) . ((ASSOC . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#58 . NIL . DEFINED .)) ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST) . NIL . (LISPAX#58) . NIL . LISPAX . NIL . 58 .)(|∀X ALIST.SEXP ASSOC(X,ALIST)| . (AXIOM (TM& . |∀X ALIST.SEXP ASSOC(X,ALIST)|)) . (ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST ASSOC) . NIL . (LISPAX#59) . NIL . LISPAX . NIL . 59 .)(NIL . (DECL MEMBER (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((MEMBER . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#60 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 60 .)(|∀X Y U.¬MEMBER(X,NIL)∧MEMBER(X,Y.U)=(X=Y∨MEMBER(X,U))| . (DEFAX MEMBER (TM& . |∀X Y U.¬MEMBER(X,NIL)∧MEMBER(X,Y.U)=(X=Y∨MEMBER(X,U))|)) . ((MEMBER . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#61 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#61) . NIL . LISPAX . NIL . 61 .)(|∀P P1 P2 B.(ATOM P⊃ SUBLIS(P,B)= (IF ISVAR P THEN (IF NULL ASSOC(P,B) THEN NIL ELSE CDR ASSOC(P,B)) ELSE P))∧SUBLIS(P1.P2,B)=SUBLIS(P1,B).SUBLIS(P2,B)| . (DEFINE SUBLIS (TM& . |∀P P1 P2 B.(ATOM P⊃ SUBLIS(P,B)= (IF ISVAR P THEN (IF NULL ASSOC(P,B) THEN NIL ELSE CDR ASSOC(P,B)) ELSE P))∧SUBLIS(P1.P2,B)=SUBLIS(P1,B).SUBLIS(P2,B)|) (USE (LR& LISPAX#34))) . ((SUBLIS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . MATCH#8 . NIL . DEFINED .)) CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA CONS ALIST ASSOC ISVAR P2 P1 P B2 B1 B) . NIL . (MATCH#8 LISPAX#34 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59) . NIL . MATCH . NIL . 8 .)(|∀X Y.(ATOM X⊃ MATCHFUN(X)= (λE B.(IF ISVAR X THEN (IF NULL ASSOC(X,B) THEN (X.E).B ELSE (IF CDR ASSOC(X,B)=E THEN B ELSE NO)) ELSE (IF X=E THEN B ELSE NO))))∧ MATCHFUN(X.Y)= (λE B.(IF ATOM E THEN NO ELSE (IF (MATCHFUN(X))(CAR E,B)=NO THEN NO ELSE (MATCHFUN(Y))(CDR E,(MATCHFUN(X))(CAR E,B)))))| . (DEFINE MATCHFUN (TM& . |∀X Y.(ATOM X⊃ MATCHFUN(X)= (λE B.(IF ISVAR X THEN (IF NULL ASSOC(X,B) THEN (X.E).B ELSE (IF CDR ASSOC(X,B)=E THEN B ELSE NO)) ELSE (IF X=E THEN B ELSE NO))))∧ MATCHFUN(X.Y)= (λE B.(IF ATOM E THEN NO ELSE (IF (MATCHFUN(X))(CAR E,B)=NO THEN NO ELSE (MATCHFUN(Y))(CDR E,(MATCHFUN(X))(CAR E,B)))))|) (USE (LR& LISPAX#38) UE: (UELST& (BIGFUN . |λX Y ARB1 ARB2.(λE B.(IF ATOM E THEN NO ELSE (IF ARB1(CAR E,B)=NO THEN NO ELSE ARB2(CDR E,ARB1(CAR E,B)))))|)))) . ((MATCHFUN . (|GROUND→((GROUND⊗GROUND)→GROUND)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . MATCH#9 . NIL . DEFINED .)) CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC ISVAR E2 E1 E B2 B1 B NO) . NIL . (MATCH#9 LISPAX#38 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59) . NIL . MATCH . NIL . 9 .)(|∀P E B.MATCH(P,E,B)=(MATCHFUN(P))(E,B)| . (DEFINE MATCH (TM& . |∀P E B.MATCH(P,E,B)=(MATCHFUN(P))(E,B)|) NIL) . ((MATCH . (|(GROUND⊗GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . MATCH#10 . NIL . DEFINED .)) CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC ISVAR P2 P1 P E2 E1 E B2 B1 B NO MATCHFUN) . NIL . (MATCH#10 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59) . NIL . MATCH . NIL . 10 .)(|¬NULL NO| . (AXIOM (TM& . |¬NULL NO|)) . (ATOM NULL NO) . NIL . (MATCH#11) . NIL . MATCH . NIL . 11 .)(|∀X Y.¬NULL X.Y| . (AXIOM (TM& . |∀X Y.¬NULL X.Y|)) . (NULL SEXP Z Y X CONS) . NIL . (MATCH#12) . NIL . MATCH . NIL . 12 .)(|∀B.¬B=NO| . (AXIOM (TM& . |∀B.¬B=NO|)) . (ATOM ALISTP B2 B1 B NO) . NIL . (MATCH#13) . NIL . MATCH . NIL . 13 .)(|∀X Y.¬X.Y=NO| . (AXIOM (TM& . |∀X Y.¬X.Y=NO|)) . (ATOM SEXP Z Y X CONS NO) . NIL . (MATCH#14) . NIL . MATCH . NIL . 14 .)(|∀P E B.ATOM P⊃(¬MATCH(P,E,B)=NO⊃ALISTP MATCH(P,E,B))| . (DERIVE (TM& . |∀P E B.ATOM P⊃(¬MATCH(P,E,B)=NO⊃ALISTP MATCH(P,E,B))|) ((LR&)) (OPEN MATCH MATCHFUN)) . (CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCH ISVAR P2 P1 P E2 E1 E B2 B1 B NO MATCHFUN) . NIL . (MATCH#10 MATCH#9 LISPAX#38 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14) . NIL . MATCH . NIL . 15 .)(|∀X E B.¬(MATCHFUN(X))(E,B)=NO⊃ALISTP (MATCHFUN(X))(E,B)| . (UE (UELST& (PHI . |λP.(∀E B.¬MATCH(P,E,B)=NO⊃ALISTP MATCH(P,E,B))|)) (LN& . LISPAX#33) ((OPEN MATCHFUN MATCH) (USE (LR& MATCH#15)))) . (CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA PHI CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCH ISVAR P2 P1 P E2 E1 E B2 B1 B NO MATCHFUN) . NIL . (MATCH#10 MATCH#9 LISPAX#38 LISPAX#33 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14) . NIL . MATCH . NIL . 16 .)(|∀P1 P2 P3 E1 E2 E3.(MATCHFUN((P1.P2).P3))((E1.E2).E3,B)= (MATCHFUN(P1.(P2.P3)))(E1.(E2.E3),B)| . (TRW (TM& . |∀P1 P2 P3 E1 E2 E3.(MATCHFUN((P1.P2).P3))((E1.E2).E3,B)= (MATCHFUN(P1.(P2.P3)))(E1.(E2.E3),B)|) (OPEN MATCHFUN)) . (CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC ISVAR P2 P1 P E2 E1 E B2 B1 B NO MATCHFUN (E3 . (GROUND . (SYMBOL& SEXP NIL) . NIL . ((BINDP& . 1000)) . MATCH#17 . NIL . VARIABLE .)) (P3 . (GROUND . (SYMBOL& SEXP NIL) . NIL . ((BINDP& . 1000)) . MATCH#17 . NIL . VARIABLE .))) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 17 .)(|∀P1 P2 P3 E1 E2.¬ATOM E1⊃ (MATCHFUN((P1.P2).P3))(E1.E2,B)= (MATCHFUN(P1.(P2.P3)))(CAR E1.(CDR E1.E2),B)| . (TRW (TM& . |∀P1 P2 P3 E1 E2.¬ATOM E1⊃ (MATCHFUN((P1.P2).P3))(E1.E2,B)= (MATCHFUN(P1.(P2.P3)))(CAR E1.(CDR E1.E2),B)|) (USE (LR& LISPAX#26 LISPAX#27) MODE: EXACT DIRECTION: REVERSE (LR& MATCH#17))) . (CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC ISVAR P2 P1 P E2 E1 E B2 B1 B NO MATCHFUN E3 P3) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 18 .)(|∀P1 P2 E B.¬(MATCHFUN(P1.P2))(E,B)=NO⊃¬ATOM E∧¬(MATCHFUN(P1))(CAR E,B)=NO| . (TRW (TM& . |∀P1 P2 E B.¬(MATCHFUN(P1.P2))(E,B)=NO⊃¬ATOM E∧¬(MATCHFUN(P1))(CAR E,B)=NO|) (PART (PRT& 1 1) (OPEN MATCHFUN))) . (CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC ISVAR P2 P1 P E2 E1 E B2 B1 B NO MATCHFUN) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 19 .)(|∀XA YA E B.XA=YA⊃ (¬(MATCHFUN(XA))(E,B)=NO∧¬NULL ASSOC(YA,B)⊃ ASSOC(YA,(MATCHFUN(XA))(E,B))=ASSOC(YA,B))| . (DERIVE (TM& . |∀XA YA E B.XA=YA⊃ (¬(MATCHFUN(XA))(E,B)=NO∧¬NULL ASSOC(YA,B)⊃ ASSOC(YA,(MATCHFUN(XA))(E,B))=ASSOC(YA,B))|) ((LR&)) (OPEN MATCHFUN)) . (CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC ISVAR E2 E1 E B2 B1 B NO MATCHFUN) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 20 .)(|∀XA YA E B.¬XA=YA⊃ (¬(MATCHFUN(XA))(E,B)=NO∧¬NULL ASSOC(YA,B)⊃ ASSOC(YA,(MATCHFUN(XA))(E,B))=ASSOC(YA,B))| . (DERIVE (TM& . |∀XA YA E B.¬XA=YA⊃ (¬(MATCHFUN(XA))(E,B)=NO∧¬NULL ASSOC(YA,B)⊃ ASSOC(YA,(MATCHFUN(XA))(E,B))=ASSOC(YA,B))|) ((LR&)) (OPEN MATCHFUN)) . (CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC ISVAR E2 E1 E B2 B1 B NO MATCHFUN) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 21 .)(|∀XA YA E B.¬(MATCHFUN(XA))(E,B)=NO∧¬NULL ASSOC(YA,B)⊃ ASSOC(YA,(MATCHFUN(XA))(E,B))=ASSOC(YA,B)| . (DERIVE (TM& . |∀XA YA E B.¬(MATCHFUN(XA))(E,B)=NO∧¬NULL ASSOC(YA,B)⊃ ASSOC(YA,(MATCHFUN(XA))(E,B))=ASSOC(YA,B)|) ((LR& MATCH#21 MATCH#20)) NIL) . (CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC ISVAR E2 E1 E B2 B1 B NO MATCHFUN) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 22 .)(|(∀X Y.(∀XA E B.¬(MATCHFUN(X))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃ ASSOC(XA,(MATCHFUN(X))(E,B))=ASSOC(XA,B))∧ (∀XA E B.¬(MATCHFUN(Y))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃ ASSOC(XA,(MATCHFUN(Y))(E,B))=ASSOC(XA,B))⊃ (∀XA E B.¬(MATCHFUN(X.Y))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃ ASSOC(XA,(MATCHFUN(X.Y))(E,B))=ASSOC(XA,B)))⊃(∀X XA E B.¬(MATCHFUN(X))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃ ASSOC(XA,(MATCHFUN(X))(E,B))=ASSOC(XA,B))| . (UE (UELST& (PHI . |λP.(∀XA E B.¬MATCH(P,E,B)=NO∧¬NULL ASSOC(XA,B)⊃ ASSOC(XA,MATCH(P,E,B))=ASSOC(XA,B))|)) (LN& . LISPAX#33) ((USE (LR& MATCH#22)) (OPEN MATCH))) . (CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA PHI CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCH ISVAR P2 P1 P E2 E1 E B2 B1 B NO MATCHFUN) . NIL . (MATCH#9 LISPAX#38 MATCH#10 LISPAX#33 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 23 .)(|∀XA E B.¬(MATCHFUN(X))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃ ASSOC(XA,(MATCHFUN(X))(E,B))=ASSOC(XA,B)| . (ASSUME (TM& . |∀XA E B.¬(MATCHFUN(X))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃ ASSOC(XA,(MATCHFUN(X))(E,B))=ASSOC(XA,B)|)) . (CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC ISVAR E2 E1 E B2 B1 B NO MATCHFUN) . NIL . (MATCH#24) . NIL . MATCH . NIL . 24 .)(|∀XA E B.¬(MATCHFUN(Y))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃ ASSOC(XA,(MATCHFUN(Y))(E,B))=ASSOC(XA,B)| . (ASSUME (TM& . |∀XA E B.¬(MATCHFUN(Y))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃ ASSOC(XA,(MATCHFUN(Y))(E,B))=ASSOC(XA,B)|)) . (CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC ISVAR E2 E1 E B2 B1 B NO MATCHFUN) . NIL . (MATCH#25) . NIL . MATCH . NIL . 25 .)(|¬(MATCHFUN(X.Y))(E,B)=NO∧¬NULL ASSOC(XA,B)| . (ASSUME (TM& . |¬(MATCHFUN(X.Y))(E,B)=NO∧¬NULL ASSOC(XA,B)|)) . (CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC ISVAR E2 E1 E B2 B1 B NO MATCHFUN) . NIL . (MATCH#26) . NIL . MATCH . NIL . 26 .)(|¬(ATOM E∨(MATCHFUN(X))(CAR E,B)=NO∨ (MATCHFUN(Y))(CDR E,(MATCHFUN(X))(CAR E,B))=NO)∧¬NULL ASSOC(XA,B)| . (RW (LN& . MATCH#26) (OPEN MATCHFUN)) . (CAR CDR ATOM NULL ALISTP SEXP Y X XA ASSOC E B NO MATCHFUN) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 MATCH#26 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 27 .)(|ASSOC(XA,(MATCHFUN(X))(CAR E,B))=ASSOC(XA,B)| . (UE (UELST& (XA . XA) (E . |CAR E|) (B . B)) (LN& . MATCH#24) (USE (LR& MATCH#27))) . (CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC ISVAR E2 E1 E B2 B1 B NO MATCHFUN) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 MATCH#26 MATCH#24 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 28 .)(|ASSOC(XA,(MATCHFUN(Y))(CDR E,(MATCHFUN(X))(CAR E,B)))=ASSOC(XA,B)| . (UE (UELST& (XA . XA) (E . |CDR E|) (B . |(MATCHFUN(X))(CAR E,B)|)) (LN& . MATCH#25) (USE (LR& MATCH#28) (LR& MATCH#27))) . (CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC ISVAR E2 E1 E B2 B1 B NO MATCHFUN) . NIL . (MATCH#24 MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 MATCH#26 MATCH#25 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 29 .)(|ASSOC(XA,(MATCHFUN(X.Y))(E,B))=ASSOC(XA,B)| . (TRW (TM& . |ASSOC(XA,(MATCHFUN(X.Y))(E,B))=ASSOC(XA,B)|) ((OPEN MATCHFUN) (USE (LR& MATCH#29) (LR& MATCH#27)))) . (CAR CDR ATOM NULL ALISTP SEXP Z Y X ZA YA XA CONS ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC ISVAR E2 E1 E B2 B1 B NO MATCHFUN) . NIL . (MATCH#24 MATCH#25 MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 MATCH#26 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 30 .)(|¬(MATCHFUN(X.Y))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃ASSOC(XA,(MATCHFUN(X.Y))(E,B))=ASSOC(XA,B)| . (CI ((LR& MATCH#26)) (LN& . MATCH#30) NIL) . (ATOM NULL ALISTP SEXP Y X XA CONS ASSOC E B NO MATCHFUN) . NIL . (LISPAX#38 MATCH#9 LISPAX#33 MATCH#10 MATCH#25 MATCH#24 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 31 .)(|(∀XA E B.¬(MATCHFUN(X))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃ ASSOC(XA,(MATCHFUN(X))(E,B))=ASSOC(XA,B))∧(∀XA E B.¬(MATCHFUN(Y))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃ ASSOC(XA,(MATCHFUN(Y))(E,B))=ASSOC(XA,B))⊃(¬(MATCHFUN(X.Y))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃ ASSOC(XA,(MATCHFUN(X.Y))(E,B))=ASSOC(XA,B))| . (CI ((LR& MATCH#24 MATCH#25)) (LN& . MATCH#31) NIL) . (ATOM NULL ALISTP SEXP Y X XA CONS ASSOC E B NO MATCHFUN) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 32 .)(|∀X XA E B.¬(MATCHFUN(X))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃ ASSOC(XA,(MATCHFUN(X))(E,B))=ASSOC(XA,B)| . (RW (LN& . MATCH#23) (USE (LR& MATCH#32))) . (ATOM NULL ALISTP SEXP X XA ASSOC E B NO MATCHFUN) . NIL . (MATCH#9 LISPAX#38 MATCH#10 LISPAX#33 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 33 .)(|(∀X.ATOM X⊃ (∀P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃ E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B))))∧(∀X Y.(∀P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃ E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B)))∧ (∀P2 E1 E2 B.¬(MATCHFUN(Y.P2))(E1.E2,B)=NO⊃ E1=SUBLIS(Y,(MATCHFUN(Y.P2))(E1.E2,B)))⊃ (∀P2 E1 E2 B.¬(MATCHFUN((X.Y).P2))(E1.E2,B)=NO⊃ E1=SUBLIS(X.Y,(MATCHFUN((X.Y).P2))(E1.E2,B))))⊃(∀X P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃ E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B)))| . (UE (UELST& (PHI . |λP1.(∀P2 E1 E2 B.¬MATCH(P1.P2,E1.E2,B)=NO⊃E1=SUBLIS(P1,MATCH(P1.P2,E1.E2,B)))|)) (LN& . LISPAX#33) (OPEN MATCH)) . (CAR CDR ATOM NULL ALISTP SEXP SUBLIS MATCH ISVAR Z Y X ZA YA XA PHI CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#9 LISPAX#38 MATCH#10 LISPAX#33 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 34 .)(|∀P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃ E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B))| . (ASSUME (TM& . |∀P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃ E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B))|)) . (CAR CDR ATOM NULL ALISTP SEXP SUBLIS ISVAR Z Y X ZA YA XA CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#35) . NIL . MATCH . NIL . 35 .)(|∀P2 E1 E2 B.¬(MATCHFUN(Y.P2))(E1.E2,B)=NO⊃ E1=SUBLIS(Y,(MATCHFUN(Y.P2))(E1.E2,B))| . (ASSUME (TM& . |∀P2 E1 E2 B.¬(MATCHFUN(Y.P2))(E1.E2,B)=NO⊃ E1=SUBLIS(Y,(MATCHFUN(Y.P2))(E1.E2,B))|)) . (CAR CDR ATOM NULL ALISTP SEXP SUBLIS ISVAR Z Y X ZA YA XA CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#36) . NIL . MATCH . NIL . 36 .)(|¬(MATCHFUN((X.Y).P2))(E1.E2,B)=NO| . (ASSUME (TM& . |¬(MATCHFUN((X.Y).P2))(E1.E2,B)=NO|)) . (CAR CDR ATOM NULL ALISTP SEXP ISVAR Z Y X ZA YA XA CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#37) . NIL . MATCH . NIL . 37 .)(|¬(MATCHFUN(X.Y))(E1,B)=NO| . (UE (UELST& (P1 . |X.Y|) (P2 . P2) (E . |E1.E2|) (B . B)) (LN& . MATCH#19) (USE (LR& MATCH#37))) . (CAR CDR ATOM NULL ALISTP SEXP ISVAR Z Y X ZA YA XA CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#37 MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 38 .)(|¬ATOM E1∧¬(MATCHFUN(X))(CAR E1,B)=NO| . (UE (UELST& (P1 . X) (P2 . Y) (E . E1) (B . B)) (LN& . MATCH#19) (USE (LR& MATCH#38) (LR& MATCH#37))) . (CAR CDR ATOM NULL ALISTP SEXP ISVAR Z Y X ZA YA XA CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#37 MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 39 .)(|¬(MATCHFUN(X.(Y.P2)))(CAR E1.(CDR E1.E2),B)=NO| . (RW (LN& . MATCH#37) (USE (LR& MATCH#38 MATCH#39) (LR& MATCH#18) MODE: EXACT)) . (CAR CDR ATOM ALISTP SEXP Y X CONS P2 E2 E1 B NO MATCHFUN) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 MATCH#37 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 40 .)(|¬(MATCHFUN(Y.P2))(CDR E1.E2,(MATCHFUN(X))(CAR E1,B))=NO| . (RW (LN& . MATCH#40) ((USE (LR& MATCH#38 MATCH#39 MATCH#40)) (NUSE (LR& MATCH#40)) (PART (PRT& 1 1 0) (OPEN MATCHFUN)))) . (CAR CDR ATOM ALISTP SEXP Y X CONS P2 E2 E1 B NO MATCHFUN) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 MATCH#37 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 41 .)(|CAR E1=SUBLIS(X,(MATCHFUN((X.Y).P2))(E1.E2,B))| . (UE (UELST& (P2 . |Y.P2|) (E1 . |CAR E1|) (E2 . |CDR E1.E2|) (B . B)) (LN& . MATCH#35) (USE (LR& MATCH#17) DIRECTION: REVERSE MODE: EXACT)) . (CAR CDR ATOM NULL ALISTP SEXP SUBLIS ISVAR Z Y X ZA YA XA CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 MATCH#35 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16 MATCH#37 MATCH#38 MATCH#39 MATCH#40 MATCH#41) . NIL . MATCH . NIL . 42 .)(|CDR E1=SUBLIS(Y,(MATCHFUN(Y.P2))(CDR E1.E2,(MATCHFUN(X))(CAR E1,B)))| . (UE (UELST& (P2 . P2) (E1 . |CDR E1|) (E2 . E2) (B . |(MATCHFUN(X))(CAR E1,B)|)) (LN& . MATCH#36) NIL) . (CAR CDR ATOM NULL ALISTP SEXP SUBLIS ISVAR Z Y X ZA YA XA CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#10 MATCH#9 LISPAX#38 LISPAX#33 MATCH#36 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16 MATCH#37 MATCH#38 MATCH#39 MATCH#40 MATCH#41) . NIL . MATCH . NIL . 43 .)(|E1=SUBLIS(X.Y,(MATCHFUN((X.Y).P2))(E1.E2,B))≡E1=SUBLIS(X,(MATCHFUN((X.Y).P2))(E1.E2,B)).SUBLIS(Y,(MATCHFUN((X.Y).P2))(E1.E2,B))| . (TRW (TM& . |E1=SUBLIS(X.Y,(MATCHFUN((X.Y).P2))(E1.E2,B))|) (OPEN SUBLIS)) . (CAR CDR ATOM NULL ALISTP SEXP SUBLIS ISVAR Z Y X ZA YA XA CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#10 MATCH#9 LISPAX#38 LISPAX#33 MATCH#8 LISPAX#34 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16 MATCH#37 MATCH#38 MATCH#39 MATCH#40 MATCH#41) . NIL . MATCH . NIL . 44 .)(|E1=SUBLIS(X.Y,(MATCHFUN((X.Y).P2))(E1.E2,B))≡E1=SUBLIS(X,(MATCHFUN((X.Y).P2))(E1.E2,B)).SUBLIS(Y,(MATCHFUN(X.(Y.P2)))(CAR E1.(CDR E1.E2),B))| . (RW (LN& . MATCH#44) (PART (PRT& 2 2 2) (USE (LR& MATCH#18) MODE: EXACT))) . (CAR CDR ALISTP SEXP SUBLIS Y X CONS P2 E2 E1 B MATCHFUN) . NIL . (MATCH#10 MATCH#9 LISPAX#38 LISPAX#33 MATCH#8 LISPAX#34 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16 MATCH#37 MATCH#38 MATCH#39 MATCH#40 MATCH#41) . NIL . MATCH . NIL . 45 .)(|E1=SUBLIS(X.Y,(MATCHFUN((X.Y).P2))(E1.E2,B))≡E1=SUBLIS(X,(MATCHFUN((X.Y).P2))(E1.E2,B)).SUBLIS(Y,(MATCHFUN(Y.P2))(CDR E1.E2,(MATCHFUN(X))(CAR E1,B)))| . (RW (LN& . MATCH#45) (PART (PRT& 2 2 2 2 0) (OPEN MATCHFUN))) . (CAR CDR ALISTP SEXP SUBLIS Y X CONS P2 E2 E1 B MATCHFUN) . NIL . (MATCH#10 MATCH#9 LISPAX#38 LISPAX#33 MATCH#8 LISPAX#34 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16 MATCH#37 MATCH#38 MATCH#39 MATCH#40 MATCH#41) . NIL . MATCH . NIL . 46 .)(|E1=SUBLIS(X.Y,(MATCHFUN((X.Y).P2))(E1.E2,B))| . (RW (LN& . MATCH#46) ((USE (LR& MATCH#42) MODE: EXACT DIRECTION: REVERSE) (USE (LR& MATCH#43) MODE: EXACT DIRECTION: REVERSE))) . (ALISTP SEXP SUBLIS Y X CONS P2 E2 E1 B MATCHFUN) . NIL . (MATCH#35 MATCH#36 MATCH#10 MATCH#9 LISPAX#38 LISPAX#33 MATCH#8 LISPAX#34 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16 MATCH#37 MATCH#38 MATCH#39 MATCH#40 MATCH#41) . NIL . MATCH . NIL . 47 .)(|¬(MATCHFUN((X.Y).P2))(E1.E2,B)=NO⊃E1=SUBLIS(X.Y,(MATCHFUN((X.Y).P2))(E1.E2,B))| . (CI ((LR& MATCH#37)) (LN& . MATCH#47) NIL) . (ATOM ALISTP SEXP SUBLIS Y X CONS P2 E2 E1 B NO MATCHFUN) . NIL . (MATCH#41 MATCH#40 MATCH#39 MATCH#38 LISPAX#34 MATCH#8 LISPAX#33 LISPAX#38 MATCH#9 MATCH#10 MATCH#36 MATCH#35 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 48 .)(|(∀P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃ E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B)))∧(∀P2 E1 E2 B.¬(MATCHFUN(Y.P2))(E1.E2,B)=NO⊃ E1=SUBLIS(Y,(MATCHFUN(Y.P2))(E1.E2,B)))⊃(¬(MATCHFUN((X.Y).P2))(E1.E2,B)=NO⊃ E1=SUBLIS(X.Y,(MATCHFUN((X.Y).P2))(E1.E2,B)))| . (CI ((LR& MATCH#35 MATCH#36)) (LN& . MATCH#48) NIL) . (ATOM ALISTP SEXP SUBLIS Y X CONS P2 E2 E1 B NO MATCHFUN) . NIL . (MATCH#10 MATCH#9 LISPAX#38 LISPAX#33 MATCH#8 LISPAX#34 MATCH#38 MATCH#39 MATCH#40 MATCH#41 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 49 .)(|(∀X.ATOM X⊃ (∀P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃ E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B))))⊃(∀X P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃ E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B)))| . (RW (LN& . MATCH#34) (USE (LR& MATCH#49))) . (ATOM ALISTP SEXP SUBLIS X CONS P2 E2 E1 B NO MATCHFUN) . NIL . (MATCH#8 LISPAX#34 MATCH#38 MATCH#39 MATCH#40 MATCH#41 MATCH#9 LISPAX#38 MATCH#10 LISPAX#33 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 50 .)(|∀X.ATOM X⊃ (∀P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃ E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B)))| . (DERIVE (TM& . |∀X.ATOM X⊃ (∀P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃ E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B)))|) ((LR& MATCH#33)) ((PART (PRT& 1 2 1 1) (OPEN MATCHFUN)) (OPEN SUBLIS))) . (CAR CDR ATOM NULL ALISTP SEXP SUBLIS ISVAR Z Y X ZA YA XA CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#8 LISPAX#34 MATCH#9 LISPAX#38 MATCH#10 LISPAX#33 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 51 .)(|∀X P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃ E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B))| . (RW (LN& . MATCH#50) (USE (LR& MATCH#51))) . (ATOM ALISTP SEXP SUBLIS X CONS P2 E2 E1 B NO MATCHFUN) . NIL . (MATCH#8 LISPAX#34 MATCH#38 MATCH#39 MATCH#40 MATCH#41 MATCH#9 LISPAX#38 MATCH#10 LISPAX#33 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 52 .)(|∀P E B.ATOM P⊃(MATCHFUN(P))(E,B)=NO∨E=SUBLIS(P,(MATCHFUN(P))(E,B))| . (TRW (TM& . |∀P E B.ATOM P⊃(MATCHFUN(P))(E,B)=NO∨E=SUBLIS(P,(MATCHFUN(P))(E,B))|) (OPEN MATCHFUN SUBLIS)) . (CAR CDR ATOM NULL ALISTP SEXP SUBLIS ISVAR Z Y X ZA YA XA CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 MATCH#8 LISPAX#34 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 53 .)(|∀P.ATOM P⊃(∀E B.¬(MATCHFUN(P))(E,B)=NO⊃E=SUBLIS(P,(MATCHFUN(P))(E,B)))| . (DERIVE (TM& . |∀P.ATOM P⊃(∀E B.¬(MATCHFUN(P))(E,B)=NO⊃E=SUBLIS(P,(MATCHFUN(P))(E,B)))|) ((LR& MATCH#53)) NIL) . (CAR CDR ATOM NULL ALISTP SEXP SUBLIS ISVAR Z Y X ZA YA XA CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 MATCH#8 LISPAX#34 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 54 .)(|(∀X.ATOM X⊃(∀E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B))))∧(∀X Y.(∀E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B)))∧ (∀E B.¬(MATCHFUN(Y))(E,B)=NO⊃E=SUBLIS(Y,(MATCHFUN(Y))(E,B)))⊃ (∀E B.¬(MATCHFUN(X.Y))(E,B)=NO⊃E=SUBLIS(X.Y,(MATCHFUN(X.Y))(E,B))))⊃(∀X E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B)))| . (UE (UELST& (PHI . |λP.(∀E B.¬MATCH(P,E,B)=NO⊃E=SUBLIS(P,MATCH(P,E,B)))|)) (LN& . LISPAX#33) (OPEN MATCH)) . (CAR CDR ATOM NULL ALISTP SEXP SUBLIS MATCH ISVAR Z Y X ZA YA XA PHI CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#9 LISPAX#38 MATCH#10 LISPAX#33 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 55 .)(|(∀X Y.(∀E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B)))∧ (∀E B.¬(MATCHFUN(Y))(E,B)=NO⊃E=SUBLIS(Y,(MATCHFUN(Y))(E,B)))⊃ (∀E B.¬(MATCHFUN(X.Y))(E,B)=NO⊃E=SUBLIS(X.Y,(MATCHFUN(X.Y))(E,B))))⊃(∀X E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B)))| . (RW (LN& . MATCH#55) (USE (LR& MATCH#54))) . (ATOM ALISTP SEXP SUBLIS Y X CONS E B NO MATCHFUN) . NIL . (MATCH#8 LISPAX#34 MATCH#9 LISPAX#38 MATCH#10 LISPAX#33 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 56 .)(|(∀E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B)))∧(∀E B.¬(MATCHFUN(Y))(E,B)=NO⊃E=SUBLIS(Y,(MATCHFUN(Y))(E,B)))| . (ASSUME (TM& . |(∀E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B)))∧(∀E B.¬(MATCHFUN(Y))(E,B)=NO⊃E=SUBLIS(Y,(MATCHFUN(Y))(E,B)))|)) . (CAR CDR ATOM NULL ALISTP SEXP SUBLIS ISVAR Z Y X ZA YA XA CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#57) . NIL . MATCH . NIL . 57 .)(|¬(MATCHFUN(X.Y))(E,B)=NO| . (ASSUME (TM& . |¬(MATCHFUN(X.Y))(E,B)=NO|)) . (CAR CDR ATOM NULL ALISTP SEXP ISVAR Z Y X ZA YA XA CONS E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#58) . NIL . MATCH . NIL . 58 .)(|¬(ATOM E∨(MATCHFUN(X))(CAR E,B)=NO∨ (MATCHFUN(Y))(CDR E,(MATCHFUN(X))(CAR E,B))=NO)| . (RW (LN& . MATCH#58) (OPEN MATCHFUN)) . (CAR CDR ATOM ALISTP SEXP Y X E B NO MATCHFUN) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 MATCH#58 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 59 .)(|CDR E=SUBLIS(Y,(MATCHFUN(Y))(CDR E,(MATCHFUN(X))(CAR E,B)))| . (TRW (TM& . |CDR E=SUBLIS(Y,(MATCHFUN(Y))(CDR E,(MATCHFUN(X))(CAR E,B)))|) (USE (LR& MATCH#57) (LR& MATCH#58) (LR& MATCH#59))) . (CAR CDR ATOM NULL ALISTP SEXP SUBLIS ISVAR Z Y X ZA YA XA CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#57 MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 MATCH#58 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 60 .)(|E=CAR E.CDR E| . (TRW (TM& . |E=CAR E.CDR E|) ((USE (LR& MATCH#59)) (USE (LR& LISPAX#26 LISPAX#27) DIRECTION: REVERSE))) . (CAR CDR SEXP CONS E2 E1 E) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 MATCH#58 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 61 .)(|¬(MATCHFUN(X.Y))(CAR E.CDR E,B)=NO| . (RW (LN& . MATCH#58) ((NUSE (LR& LISPAX#26 LISPAX#27)) (USE (LR& MATCH#61) MODE: EXACT))) . (CAR CDR ATOM ALISTP SEXP Y X CONS E B NO MATCHFUN) . NIL . (MATCH#10 LISPAX#33 MATCH#9 LISPAX#38 MATCH#58 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 62 .)(|CAR E=SUBLIS(X,(MATCHFUN(X.Y))(E,B))| . (UE (UELST& (X . X) (P2 . Y) (E1 . |CAR E|) (E2 . |CDR E|) (B . B)) (LN& . MATCH#52) (USE (LR& MATCH#59) (LR& MATCH#62))) . (CAR CDR ATOM NULL ALISTP SEXP SUBLIS ISVAR Z Y X ZA YA XA CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#58 MATCH#8 LISPAX#34 MATCH#38 MATCH#39 MATCH#40 MATCH#41 MATCH#9 LISPAX#38 MATCH#10 LISPAX#33 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 63 .)(|E=SUBLIS(X.Y,(MATCHFUN(X.Y))(E,B))≡E=SUBLIS(X,(MATCHFUN(X.Y))(E,B)).SUBLIS(Y,(MATCHFUN(X.Y))(E,B))| . (TRW (TM& . |E=SUBLIS(X.Y,(MATCHFUN(X.Y))(E,B))|) ((USE (LR& MATCH#58)) (OPEN SUBLIS))) . (CAR CDR ATOM NULL ALISTP SEXP SUBLIS ISVAR Z Y X ZA YA XA CONS P2 P1 P E2 E1 E B2 B1 B NO ARB2 ARB1 ARB BIGFUN ATOM_FUN DEFINED_FUN ALIST ASSOC MATCHFUN) . NIL . (MATCH#10 MATCH#9 LISPAX#38 LISPAX#33 MATCH#58 MATCH#8 LISPAX#34 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 64 .)(|E=SUBLIS(X.Y,(MATCHFUN(X.Y))(E,B))≡E=CAR E.SUBLIS(Y,(MATCHFUN(Y))(CDR E,(MATCHFUN(X))(CAR E,B)))| . (RW (LN& . MATCH#64) ((USE (LR& MATCH#58) (LR& MATCH#59)) (PART (PRT& 2 2 1) (USE (LR& MATCH#63) MODE: EXACT DIRECTION: REVERSE)) (PART (PRT& 2 2 2 2 0) (OPEN MATCHFUN)))) . (CAR CDR ALISTP SEXP SUBLIS Y X CONS E B MATCHFUN) . NIL . (MATCH#38 MATCH#39 MATCH#40 MATCH#41 MATCH#10 MATCH#9 LISPAX#38 LISPAX#33 MATCH#58 MATCH#8 LISPAX#34 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 65 .)(|E=SUBLIS(X.Y,(MATCHFUN(X.Y))(E,B))| . (RW (LN& . MATCH#65) ((USE (LR& MATCH#59)) (PART (PRT& 2 2 2) (USE (LR& MATCH#60) DIRECTION: REVERSE)))) . (ALISTP SEXP SUBLIS Y X CONS E B MATCHFUN) . NIL . (MATCH#57 MATCH#38 MATCH#39 MATCH#40 MATCH#41 MATCH#10 MATCH#9 LISPAX#38 LISPAX#33 MATCH#58 MATCH#8 LISPAX#34 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 66 .)(|¬(MATCHFUN(X.Y))(E,B)=NO⊃E=SUBLIS(X.Y,(MATCHFUN(X.Y)(αU,B))| . (CI ((LR& MATCH#58)) (LN& . MATCH#66) NIL) . (ATOM ALISTP SEXP SUBLIS Y X CONS E B NO MATCHFUN) . NIL . (LISPAX#34 MATCH#8 LISPAX#33 LISPAX#38 MATCH#9 MATCH#10 MATCH#41 MATCH#40 MATCH#39 MATCH#38 MATCH#57 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 67 .)(|(∀E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B)))∧(∀E B.¬(MATCHFUN(Y))(E,B)=NO⊃E=SUBLIS(Y,(MATCHFUN(Y))(E,B)))⊃(¬(MATCHFUN(X.Y))(E,B)=NO⊃E=SUBLIS(X.Y,(MATCHFUN(X.Y))(E,B)))| . (CI ((LR& MATCH#57)) (LN& . MATCH#67) NIL) . (ATOM ALISTP SEXP SUBLIS Y X CONS E B NO MATCHFUN) . NIL . (MATCH#38 MATCH#39 MATCH#40 MATCH#41 MATCH#10 MATCH#9 LISPAX#38 LISPAX#33 MATCH#8 LISPAX#34 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 68 .)(|∀X E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B))| . (RW (LN& . MATCH#56) (USE (LR& MATCH#68))) . (ATOM ALISTP SEXP SUBLIS X E B NO MATCHFUN) . NIL . (MATCH#38 MATCH#39 MATCH#40 MATCH#41 MATCH#8 LISPAX#34 MATCH#9 LISPAX#38 MATCH#10 LISPAX#33 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#56 LISPAX#58 LISPAX#55 MATCH#11 MATCH#12 MATCH#13 MATCH#14 MATCH#16) . NIL . MATCH . NIL . 69 .)